$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $m$:($T$$\rightarrow\mathbb{N}$).
\\[0ex]($\forall$$x$:$T$. $m$($f$($x$))$\leq$$m$($x$) \& ($m$($f$($x$)) $=$ $m$($x$) $\in$ $\mathbb{Z}$ $\Rightarrow$ $f$($x$) $=$ $x$)) $\Rightarrow$ ($\forall$$x$:$T$. $\exists$$n$:$\mathbb{N}$. $f$($f$$^{\mbox{\scriptsize $n$}}$($x$)) $=$ $f$$^{\mbox{\scriptsize $n$}}$($x$))